(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_IDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(assert (let ((e3 4))
(let ((e4 3))
(let ((e5 3))
(let ((e6 (>= v2 v0)))
(let ((e7 (distinct v2 v1)))
(let ((e8 (>= v1 v1)))
(let ((e9 (< (- v1 v1) e5)))
(let ((e10 (>= (- v2 v2) (- e5))))
(let ((e11 (<= v1 v0)))
(let ((e12 (= (- v2 v2) (- e5))))
(let ((e13 (> (- v2 v2) e5)))
(let ((e14 (= v1 v2)))
(let ((e15 (> v0 v2)))
(let ((e16 (distinct v1 v1)))
(let ((e17 (= v2 v2)))
(let ((e18 (>= (- v2 v0) e4)))
(let ((e19 (< (- v0 v2) e5)))
(let ((e20 (> (- v0 v2) (- e3))))
(let ((e21 (= v1 v1)))
(let ((e22 (> (- v2 v0) e4)))
(let ((e23 (distinct (- v0 v2) e5)))
(let ((e24 (= (- v2 v0) e3)))
(let ((e25 (= e14 e16)))
(let ((e26 (or e22 e17)))
(let ((e27 (or e19 e19)))
(let ((e28 (=> e13 e26)))
(let ((e29 (= e25 e27)))
(let ((e30 (=> e9 e9)))
(let ((e31 (xor e10 e29)))
(let ((e32 (ite e20 e21 e20)))
(let ((e33 (xor e11 e18)))
(let ((e34 (not e23)))
(let ((e35 (=> e12 e34)))
(let ((e36 (and e30 e24)))
(let ((e37 (or e8 e32)))
(let ((e38 (= e35 e15)))
(let ((e39 (or e31 e37)))
(let ((e40 (not e28)))
(let ((e41 (= e39 e7)))
(let ((e42 (not e33)))
(let ((e43 (= e41 e42)))
(let ((e44 (= e6 e43)))
(let ((e45 (= e36 e40)))
(let ((e46 (and e38 e38)))
(let ((e47 (and e45 e45)))
(let ((e48 (ite e44 e44 e47)))
(let ((e49 (not e48)))
(let ((e50 (and e49 e46)))
e50
)))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
